HORPO with Computability Closure: A Reconstruction
Identifieur interne : 004C56 ( Main/Exploration ); précédent : 004C55; suivant : 004C57HORPO with Computability Closure: A Reconstruction
Auteurs : Frédéric Blanqui [France] ; Jean-Pierre Jouannaud [France] ; Albert Rubio [Espagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper provides a new, decidable definition of the higher-order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability closure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.
Url:
DOI: 10.1007/978-3-540-75560-9_12
Affiliations:
- Espagne, France
- Catalogne, Grand Est, Lorraine (région), Île-de-France
- Palaiseau, Vandœuvre-lès-Nancy
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000F78
- to stream Istex, to step Curation: 000F63
- to stream Istex, to step Checkpoint: 001041
- to stream Main, to step Merge: 004D90
- to stream Main, to step Curation: 004C56
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">HORPO with Computability Closure: A Reconstruction</title><author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name></author><author><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name></author><author><name sortKey="Rubio, Albert" sort="Rubio, Albert" uniqKey="Rubio A" first="Albert" last="Rubio">Albert Rubio</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:432577477CEB5D01CDE04B3D9AE31B23E02940FE</idno><date when="2007" year="2007">2007</date><idno type="doi">10.1007/978-3-540-75560-9_12</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-0QPXGXQJ-V/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000F78</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000F78</idno><idno type="wicri:Area/Istex/Curation">000F63</idno><idno type="wicri:Area/Istex/Checkpoint">001041</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001041</idno><idno type="wicri:doubleKey">0302-9743:2007:Blanqui F:horpo:with:computability</idno><idno type="wicri:Area/Main/Merge">004D90</idno><idno type="wicri:Area/Main/Curation">004C56</idno><idno type="wicri:Area/Main/Exploration">004C56</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">HORPO with Computability Closure: A Reconstruction</title><author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>INRIA & LORIA, Protheo team, Campus Scientifique, BP 239, 54506 Vandœuvre-lès-Nancy Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author><author><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LIX, École Polytechnique, 91400 Palaiseau</wicri:regionArea><placeName><region type="region" nuts="2">Île-de-France</region><settlement type="city">Palaiseau</settlement></placeName></affiliation></author><author><name sortKey="Rubio, Albert" sort="Rubio, Albert" uniqKey="Rubio A" first="Albert" last="Rubio">Albert Rubio</name><affiliation wicri:level="2"><country xml:lang="fr">Espagne</country><wicri:regionArea>Technical University of Catalonia, Pau Gargallo 5, 08028 Barcelona</wicri:regionArea><placeName><region nuts="2" type="communauté">Catalogne</region></placeName></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper provides a new, decidable definition of the higher-order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability closure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.</div></front></TEI><affiliations><list><country><li>Espagne</li><li>France</li></country><region><li>Catalogne</li><li>Grand Est</li><li>Lorraine (région)</li><li>Île-de-France</li></region><settlement><li>Palaiseau</li><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name></region><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name></country><country name="Espagne"><region name="Catalogne"><name sortKey="Rubio, Albert" sort="Rubio, Albert" uniqKey="Rubio A" first="Albert" last="Rubio">Albert Rubio</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004C56 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004C56 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:432577477CEB5D01CDE04B3D9AE31B23E02940FE
|texte= HORPO with Computability Closure: A Reconstruction
}}
| This area was generated with Dilib version V0.6.33. |  |